es:ES{i}, i:Id, L:IdLnk List, T:(IdType{i}).
es-secret-server{table:ut2, encrypt:ut2, decrypt:ut2}(es; T; L; i)  Prop{i'} 

latex

Definitions

x:AB(x), ES, 1of(t), E, {x:A| B(x) }, , , t  T, ptr(tab), x when e, AB, #$n, x:A. B(x), a<b, Void, x:AB(x), P  Q, False, A, Atom$n, Id, type List, A & B, @i only events in L change   x : T, s = t, if b t else f fi, b, atoms-distinct(tab), Type, P & Q, Prop, first(e), i >> a, st-atom(tab;n), ||tab|| , loc(e), x. t(x), e@i. P(e), "$x", e copies x, IdLnk, lnk-inv(l), rcv(l,tg), kind(e), Knd, left+right, P  Q, (xL.P(x)), e leaks x to e', x:A. B(x), secret-table(T), x.A(x), x : v, State(ds), data(T), IdDeq, x:A. B(x), Top, f(x)?z, f(a), s.x, encrypt(tab;keyv), DeclaredType(ds;x), @i events of kind k change x to f State(ds) (val:T), xL. P(x), <a,b>, map(f;as), EqDecider(T), source(l), vartype(i;x), valtype(e), next(tab), Unit, state dsk:A sends [tg, e.f(e):B] on l, val(e), decrypt(tab;kval), destination(l), let x = a in b(x), es-secret-server, {i..j}, S  T, i  j < k

Lemmas

st-atoms-distinct wf, st-ptr wf, st-atom wf, st-next wf, int seg wf, st-length wf, unit wf, event system wf, ldst wf, st-decrypt wf, es-when wf, es-val wf, es-kind-sends-iff wf, es-valtype wf, es-vartype wf, lsrc wf, fpf-cap wf, deq wf, top wf, frame-p wf, map wf, l all wf, effect-p wf, fpf-cap-single1, st-encrypt wf, fpf-cap-single, eqof eq btrue, id-deq wf, subtype rel self, data wf, decl-state wf, fpf-single wf, secret-table wf, es-leaks wf, l exists wf, Knd wf, es-kind wf, rcv wf, lnk-inv wf, IdLnk wf, event system-level-subtype, not wf, es-copies wf, alle-at wf, es-loc wf, es-E wf, es-atom wf, Id wf, assert wf, es-first wf, nat wf, le wf